FDL - Step of Proof: decidable__equal

Step of Proof: decidable__equal_bool

9,38

Inference at * 1 2 1 1
Iof proof for Lemma decidable equal bool:

1. tt = ff

False

by ((((((MoveToConcl 1)

CollapseTHEN (Fold `not` 0))

)

CollapseTHEN (BLemma `btrue_neq_bfalse`

C))

)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 1000:n)) (first_tok :t

C) inil_term)))

Definitions P Q, False, A

Lemmas btrue neq bfalse